abstraction with a reducible body, e.g.
x . (( y . y+x) 2)
is in WHNF but not HNF. To reduce this expression to HNF
would require reduction of the lambda body:
( y . y+x) 2 --@# 2+x
The same principle is often used in
strict languages such as
expression in a lambda abstraction with no arguments:
D = delay E = () . E
The value of the expression is obtained by applying it to the
empty argument list:
force D = apply D ()
= apply ( () . E) ()
= E
(1994-10-31)